The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

active(f(x)) → mark(f(f(x)))
chk(no(f(x))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
mat(f(x), f(y)) → f(mat(x, y))
chk(no(c)) → active(c)
mat(f(x), c) → no(c)
f(active(x)) → active(f(x))
f(no(x)) → no(f(x))
f(mark(x)) → mark(f(x))
tp(mark(x)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of f: chk, f, mat
The following defined symbols can occur below the 0th argument of tp: chk, f, mat
The following defined symbols can occur below the 0th argument of chk: chk, f, mat
The following defined symbols can occur below the 0th argument of mat: chk, f, mat
The following defined symbols can occur below the 1th argument of mat: chk, f, mat

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
active(f(x)) → mark(f(f(x)))
f(active(x)) → active(f(x))

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

mat(f(x), f(y)) → f(mat(x, y))
tp(mark(x)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) → active(c)
f(no(x)) → no(f(x))
chk(no(f(x))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
f(mark(x)) → mark(f(x))
mat(f(x), c) → no(c)

Rewrite Strategy: INNERMOST

(3) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4]
transitions:
y0() → 0
mark0(0) → 0
X0() → 0
no0(0) → 0
c0() → 0
active0(0) → 0
mat0(0, 0) → 1
tp0(0) → 2
chk0(0) → 3
f0(0) → 4
X1() → 10
f1(10) → 9
f1(9) → 8
f1(8) → 8
f1(8) → 7
mat1(7, 0) → 6
chk1(6) → 5
tp1(5) → 2
c1() → 11
active1(11) → 3
f1(0) → 12
no1(12) → 4
f1(0) → 13
mark1(13) → 4
no1(12) → 12
no1(12) → 13
mark1(13) → 12
mark1(13) → 13
c1() → 14
no1(14) → 6
c2() → 15
active2(15) → 5

(4) BOUNDS(1, n^1)

(5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

mat(f(z0), f(y)) → f(mat(z0, y))
mat(f(z0), c) → no(c)
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
chk(no(c)) → active(c)
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
f(no(z0)) → no(f(z0))
f(mark(z0)) → mark(f(z0))

Tuples:

MAT(f(z0), f(y)) → c1(F(mat(z0, y)), MAT(z0, y))
MAT(f(z0), c) → c2
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
CHK(no(c)) → c4
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))

S tuples:

MAT(f(z0), f(y)) → c1(F(mat(z0, y)), MAT(z0, y))
MAT(f(z0), c) → c2
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
CHK(no(c)) → c4
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))

K tuples:none
Defined Rule Symbols:

mat, tp, chk, f

Defined Pair Symbols:

MAT, TP, CHK, F

Compound Symbols:

c1, c2, c3, c4, c5, c6, c7

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing nodes:

MAT(f(z0), f(y)) → c1(F(mat(z0, y)), MAT(z0, y))
CHK(no(c)) → c4
MAT(f(z0), c) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

mat(f(z0), f(y)) → f(mat(z0, y))
mat(f(z0), c) → no(c)
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
chk(no(c)) → active(c)
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
f(no(z0)) → no(f(z0))
f(mark(z0)) → mark(f(z0))

Tuples:

TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))

S tuples:

TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)), MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0), F(f(f(f(f(f(f(f(f(f(X)))))))))), F(f(f(f(f(f(f(f(f(X))))))))), F(f(f(f(f(f(f(f(X)))))))), F(f(f(f(f(f(f(X))))))), F(f(f(f(f(f(X)))))), F(f(f(f(f(X))))), F(f(f(f(X)))), F(f(f(X))), F(f(X)), F(X))
F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))

K tuples:none
Defined Rule Symbols:

mat, tp, chk, f

Defined Pair Symbols:

TP, CHK, F

Compound Symbols:

c3, c5, c6, c7

(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 22 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

mat(f(z0), f(y)) → f(mat(z0, y))
mat(f(z0), c) → no(c)
tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
chk(no(c)) → active(c)
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
f(no(z0)) → no(f(z0))
f(mark(z0)) → mark(f(z0))

Tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

S tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

K tuples:none
Defined Rule Symbols:

mat, tp, chk, f

Defined Pair Symbols:

F, TP, CHK

Compound Symbols:

c6, c7, c3, c5

(11) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

tp(mark(z0)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

chk(no(c)) → active(c)
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
mat(f(z0), f(y)) → f(mat(z0, y))
mat(f(z0), c) → no(c)
f(no(z0)) → no(f(z0))
f(mark(z0)) → mark(f(z0))

Tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

S tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

K tuples:none
Defined Rule Symbols:

chk, mat, f

Defined Pair Symbols:

F, TP, CHK

Compound Symbols:

c6, c7, c3, c5

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(mark(z0)) → c7(F(z0))

We considered the (Usable) Rules:

chk(no(c)) → active(c)
f(no(z0)) → no(f(z0))
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
f(mark(z0)) → mark(f(z0))

And the Tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHK(x₁)) = 0   
POL(F(x₁)) = x₁   
POL(TP(x₁)) = 0   
POL(X) = 0   
POL(active(x₁)) = 0   
POL(c) = 0   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(chk(x₁)) = 0   
POL(f(x₁)) = x₁   
POL(mark(x₁)) = [1] + x₁   
POL(mat(x₁, x₂)) = 0   
POL(no(x₁)) = x₁   
POL(y) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

chk(no(c)) → active(c)
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
mat(f(z0), f(y)) → f(mat(z0, y))
mat(f(z0), c) → no(c)
f(no(z0)) → no(f(z0))
f(mark(z0)) → mark(f(z0))

Tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

S tuples:

F(no(z0)) → c6(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

K tuples:

F(mark(z0)) → c7(F(z0))

Defined Rule Symbols:

chk, mat, f

Defined Pair Symbols:

F, TP, CHK

Compound Symbols:

c6, c7, c3, c5

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(no(z0)) → c6(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

We considered the (Usable) Rules:

chk(no(c)) → active(c)
f(no(z0)) → no(f(z0))
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
f(mark(z0)) → mark(f(z0))

And the Tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHK(x₁)) = 0   
POL(F(x₁)) = x₁   
POL(TP(x₁)) = x₁   
POL(X) = 0   
POL(active(x₁)) = 0   
POL(c) = 0   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(chk(x₁)) = 0   
POL(f(x₁)) = x₁   
POL(mark(x₁)) = [1] + x₁   
POL(mat(x₁, x₂)) = 0   
POL(no(x₁)) = [1] + x₁   
POL(y) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

chk(no(c)) → active(c)
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
mat(f(z0), f(y)) → f(mat(z0, y))
mat(f(z0), c) → no(c)
f(no(z0)) → no(f(z0))
f(mark(z0)) → mark(f(z0))

Tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

S tuples:

CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

K tuples:

F(mark(z0)) → c7(F(z0))
F(no(z0)) → c6(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

Defined Rule Symbols:

chk, mat, f

Defined Pair Symbols:

F, TP, CHK

Compound Symbols:

c6, c7, c3, c5

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

We considered the (Usable) Rules:

mat(f(z0), f(y)) → f(mat(z0, y))
chk(no(c)) → active(c)
f(no(z0)) → no(f(z0))
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
f(mark(z0)) → mark(f(z0))
mat(f(z0), c) → no(c)

And the Tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CHK(x₁)) = x₁   
POL(F(x₁)) = 0   
POL(TP(x₁)) = [2]x₁   
POL(X) = 0   
POL(active(x₁)) = 0   
POL(c) = [1]   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(chk(x₁)) = 0   
POL(f(x₁)) = [2]x₁   
POL(mark(x₁)) = x₁   
POL(mat(x₁, x₂)) = [2]x₂   
POL(no(x₁)) = [1] + x₁   
POL(y) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

chk(no(c)) → active(c)
chk(no(f(z0))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
mat(f(z0), f(y)) → f(mat(z0, y))
mat(f(z0), c) → no(c)
f(no(z0)) → no(f(z0))
f(mark(z0)) → mark(f(z0))

Tuples:

F(no(z0)) → c6(F(z0))
F(mark(z0)) → c7(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

S tuples:none
K tuples:

F(mark(z0)) → c7(F(z0))
F(no(z0)) → c6(F(z0))
TP(mark(z0)) → c3(TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))
CHK(no(f(z0))) → c5(F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0))), CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), z0)))

Defined Rule Symbols:

chk, mat, f

Defined Pair Symbols:

F, TP, CHK

Compound Symbols:

c6, c7, c3, c5

(19) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(20) BOUNDS(1, 1)